package operateurs;

import quantifieurs.PourTout;
import quantifieurs.Quantification;
import utils.FormuleType;
import utils.Symbole;
import base.Atome;
import base.Formule;

/**
 * Created by IntelliJ IDEA.
 * User: njussien
 * Date: 30/11/12
 * Time: 10:37
 */
public class Et extends OperateurBinaire {
	public Et(Formule a, Formule b) {
		this.operande = a;
		this.operandedroit = b;
	}

	public String toString() {
		//return "("+ this.operande.toString() + " ^ "+ this.operandedroit.toString()+")";
		return "("+ this.operande.toString() + " " + Symbole.ET + " "+ this.operandedroit.toString()+")";
	}

	public Formule supprimeConnecteurs() {
		return new Et(this.operande.supprimeConnecteurs(), this.operandedroit.supprimeConnecteurs());
	}

	public Formule negation() {
		return new Ou(this.operande.negation(), this.operandedroit.negation());
	}

	public Formule descendreNegation(boolean isNegatif) {
		if(isNegatif) return this.negation().descendreNegation(false);
		return new Et(this.operande.descendreNegation(false), this.operandedroit.descendreNegation(false));
	}

	public Formule transportQuantificateurs() {
		// 3) QQ x, A(x)  ^  QQ x, B(x)  -->  QQx,(A(x) ^ B(x))
		//if ((this.operande.getType() == FormuleType.POURTOUT) && (this.operandedroit.getType() == FormuleType.POURTOUT)) {
		if ((this.operande.getClass() == PourTout.class) && (this.operandedroit.getClass() == PourTout.class)) {
			Quantification formuleTmpG = (PourTout) this.operande;
			Quantification formuleTmpD = (PourTout) this.operandedroit;
			if (formuleTmpG.x.egale(formuleTmpD.x)) {
				return new PourTout(formuleTmpG.x, new Et(formuleTmpG.f, formuleTmpD.f));
			}
		}
		// 5) (QQ x, A(x)) ^ B(y)  -->  QQ x, (A(x) ^ B(y)
		//if ((this.operande.getType() == FormuleType.POURTOUT) && (this.operandedroit.getType() == FormuleType.ATOME)) {
		if ((this.operande.getClass() == PourTout.class) && (this.operandedroit.getClass() == Atome.class)) {
			Quantification formuleTmpG = (PourTout) this.operande;
			Atome formuleTmpD = (Atome) this.operandedroit;
			if (!formuleTmpG.x.egale(formuleTmpD.getOperandes()[0])) {
				return new PourTout(formuleTmpG.x, new Et(formuleTmpG.f, formuleTmpD));
			}
		}
		//if ((this.operande.getType() == FormuleType.ATOME) && (this.operandedroit.getType() == FormuleType.POURTOUT)) {
		if ((this.operande.getClass() == Atome.class) && (this.operandedroit.getClass() == PourTout.class)) {
			Atome formuleTmpG = (Atome) this.operande;
			Quantification formuleTmpD = (PourTout) this.operandedroit;
			if (!formuleTmpG.getOperandes()[0].egale(formuleTmpD.x)) {
				return new PourTout(formuleTmpD.x, new Et(formuleTmpG, formuleTmpD.f));
			}
		}
		return new Et(this.operande.transportQuantificateurs(), this.operandedroit.transportQuantificateurs());
	}

	public boolean isSame(Formule o) {
		//if (o.getType() != FormuleType.ET) return false;
		if (o.getClass() != Et.class) return false;
		Et tmp = (Et)o;
		return this.operande.isSame(tmp.operande) && this.operandedroit.isSame(tmp.operandedroit);
	}

	public Formule miseFormeClausale() {
		// TODO
		return new Et(this.operande.miseFormeClausale(), this.operandedroit.miseFormeClausale());
	}

	public FormuleType getType() {
		return FormuleType.ET;
	}
}
